a, b:, q:. a  i < b. q = (if a z b then b - a else 0 fi  * q)   

latex

Definitions	x f y, Y, t.2, t.1, 0, +r, e, *, (op,id) lb  i < ub. E(i), r+gp,  lb  i < ub. E(i), <+*>, (r) i  k < j. E(k), a  j < b. E(j), , A, x. t(x), A  B, T, ff, P  Q, P & Q, P  Q, tt, P  Q, if b then t else f fi , True, , t  T, x:A. B(x), False, x(s), Unit, , S  T,
Lemmas	qmul zero qrng, bnot of lt int, int inc rationals, int-eq-in-rationals, qmul wf, false wf, qsum-const, int seg wf, sum shift q, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, rationals wf